\begin{tabbing}
$\forall$${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $x$:ecl(${\it ds}$; ${\it da}$), ${\it es}$:event\_system\{i:l\}, $i$:Id.
\\[0ex]($\forall$$x$:Id. subtype\_rel(es{-}vartype(${\it es}$; $i$; $x$); fpf{-}cap(${\it ds}$; id{-}deq; $x$; top)))
\\[0ex]$\Rightarrow$ \=($\forall$$e$:es{-}E(${\it es}$). \+
\\[0ex](loc($e$) = $i$) $\Rightarrow$ subtype\_rel(es{-}valtype(${\it es}$; $e$); ma{-}valtype(${\it da}$; es{-}kind(${\it es}$; $e$))))
\-\\[0ex]$\Rightarrow$ \=($\forall$$n$:$\mathbb{N}$, $e_{1}$,$e_{2}$:\{$e$:es{-}E(${\it es}$)$\mid$ loc($e$) = $i$\} .\+
\\[0ex](ecl{-}es{-}halt(${\it es}$; $x$)($n$,$e_{1}$,$e_{2}$)) $\Leftarrow\!\Rightarrow$ (ecl{-}halt(${\it ds}$; ${\it da}$; $x$)($n$,es{-}hist\{i:l\}(${\it es}$;$e_{1}$;$e_{2}$))))
\-
\end{tabbing}